%We begin by introducing  our calculus, called 
%\paragraph{Basic Syntax.~}

We begin by presenting the $\evol{}$ calculus and its different variants.
Then, we introduce the operational semantics of the calculus, 
and establish the relationship
between static and dynamic topologies of adaptable processes.


\subsection{Syntax} 

The $\mathcal{E}$ calculus %in the sequel) 
is a variant of CCS \cite{Milner89} without restriction and relabeling, 
and extended with constructs for evolvability. 
As in CCS, in $\mathcal{E}$ 
processes can perform actions or synchronize on them.  
We presuppose a countable
set $\mathcal{N}$ of names, ranged over by $a,b$, possibly decorated as 
$\overline{a},  \overline{b} \ldots $ and $\til{a}, \til{b} \ldots $. 
As customary, we use $a$ and $\outC{a}$ to denote atomic input and output actions, respectively.
The syntax of $\mathcal{E}$ processes 
extends that of CCS with 
%is the following:
 primitive notions of \emph{adaptable processes} $\component{a}{P}$
 and \emph{update prefixes} $\update{a}{U}$:
 \[
P        ::=  \component{a}{P} \sepr 
          P \parallel P  \sepr \sum_{i \in I} \pi_i.P_i  \sepr ! \pi.P 
          \quad \quad \quad 
\pi   ::=  a \sepr \outC{a} \sepr \update{a}{U}
\]
Above, 
the $U$ in the update prefix
$\update{a}{U}$ is an \emph{update pattern}: it represents   
a context, i.e., a process with zero or more \emph{holes}   (see Definition \ref{d:contexts} below).
% $\mathcal{E}$ extends  CCS with \emph{update prefixes} 
%and  a primitive notion of \emph{component}. %  $\component{a}{P}$ .
%In the update prefix
%$\update{a}{P}$, 
%process $P$ represents a context, i.e., a process with a hole $\bullet$.
The intention is that when an update prefix is able to interact, 
the current state of  an adaptable process named $a$ 
is used to fill the holes in the update pattern $U$. 
Given a process $P$, 
process $\component{a}{P}$ denotes 
%the component $a$ with state $P$. 
%Alternatively, it can be seen as a 
the adaptable process $P$ \emph{located at} $a$.
Notice that $a$ acts as a \emph{transparent} locality: process $P$ can evolve on its own, and  interact freely with external processes.
Localities can be nested, so as to form suitable hierarchies of adaptable processes.
The rest of the syntax follows standard lines.
A process $\pi.P$ performs prefix $\pi$ and then behaves as $P$. 
Parallel composition $P \parallel Q$ decrees the concurrent execution of $P$ and $Q$.
We abbreviate $P_{1} \parallel \cdots \parallel P_{n}$ as $\prod_{i=1}^{n} P _{i}$, and
use $\prod^{k} P$ to denote the parallel composition of $k$ instances of process $P$.
Given an index set $I = \{1,..,n\}$, the guarded sum $\sum_{i \in I} \pi_{i}.P_{i}$ represents an exclusive choice
over $\pi_{1}.P_{1}, \ldots, \pi_{n}.P_{n}$.
As usual, we write $\pi_{1}.P_{1} + \pi_{2}.P_{2}$ if ${|}I{|}=2$, and $\nil$ if $I$ is empty. 
Process $!\, \pi.P$ defines guarded replication, i.e., 
infinitely many occurrences of $P$ in parallel, which are triggered by prefix $\pi$.
 
%We now formally define contexts. 
We now define  a general way 
of extending the grammar of process languages with holes, so as to define update patterns.
Intuitively, we extend rule productions with a hole (denoted $\bullet$), distinguishing between rule productions
for process expressions (so-called \emph{process categories}) from the rest.
In particular, we would like to avoid adding holes to rule productions for prefixes (i.e., productions for $\pi$ in the syntax).
%\todo{together with the def below, we need to make explicit the fact that we have ``process categories'' (such as $P$ and $A$) and ``non process categories'' (ie. prefixes)}

\begin{definition}\label{d:contexts}
%Let $\mathcal{L} = (N, \Sigma, R)$ define a language in terms of non-terminal symbols $N$, terminal symbols $\Sigma$,
%and rule productions $R$.
%The language $\mathcal{L}_\bullet$ is then defined as $(N_\bullet, \Sigma_\bullet, R_\bullet)$, where 
%%is obtained from $\mathcal{L}$ as follows:
%$N_\bullet = \{E_\bullet \, | \, E \in N\}$,
%$\Sigma_\bullet = \Sigma \cup \{\bullet \}$, 
%and %$P_\bullet$ is defined as
%$$R_\bullet = \{E_\bullet ::= \bullet \, | \, E_\bullet \in N_\bullet\} \cup \{E_\bullet ::= rule_\bullet \, | \, E ::= rule \in R\}$$
%where $rule_\bullet$ is obtained by replacing each non-terminal symbol $F$ in $rule$ with $F_\bullet$, 
%and leaving the terminal symbols unchanged.
% 
Given a process category $E$, we denote with $E_{\bullet}$ the process category with rule productions obtained from those of $E$ by: 
\begin{enumerate}
\item adding a new rule ``$E_{\bullet} ::= \bullet$''; 
\item replacing every rule ``$E ::= term$'' of $E$
with a rule ``$E_{\bullet} ::= term_{\bullet}$'', 
where ``$term_{\bullet}$'' is obtained from ``$term$'' by syntactically replacing all process categories $F$ occurring in ``$term$'' by $F_{\bullet}$. 
\end{enumerate}
\end{definition}
 
 Given an update pattern $U$ and a process $Q$, we define $\fillcon{U}{Q}$
 as the process obtained by filling in those holes in $U$ not occurring inside update prefixes with $Q$.


\begin{definition}\label{d:fillit}
The effect of replacing the holes in 
an update pattern $U$ with a process $Q$, %the replacement of holes in $U$ with $Q$,
denoted \fillcon{U}{Q}, 
 is defined inductively on $U$ as follows:
\begin{align*}
\fillcon{\bullet\,}{Q} &= Q & 
\fillcon{(U_{1} \parallel U_{2})}{Q} & =  \fillcon{U_{1}\,}{Q} \parallel \fillcon{U_{2}\,}{Q} \\
\fillcon{\component{a}{U}}{Q} &= \component{a}{\fillcon{U}{Q}} &
\fillcon{\bigg(\sum_{i \in I}\pi_{i}.U_{i}\bigg)}{Q} &= \sum_{i \in I}\pi_{i}.\fillcon{U_{i}\,}{Q} \\
\fillcon{(! \pi.U)}{Q} &= !\pi.(\fillcon{U}{Q})
\end{align*}
\end{definition}

This way, $\{ \cdot \}$ can be intuitively seen as a scope delimiter for holes $\bullet$  in $\update{a}{U}$.
%\add{in other terms ``$\{, \}$ delimit the scope of $\bullet$ in $\update{a}{U}$.}
Indeed, it is worth observing that Definition \ref{d:fillit} does not replace holes inside prefixes; 
this ensures a consistent treatment of nested update actions.

We now move on to consider different variants of this basic syntax by means of two different characterizations.

\paragraph{A Structural Characterization of Update}
As anticipated in the Introduction, 
our structural characterization of update in
$\mathcal{E}$ 
defines
two families of languages,
%derived from $\mathcal{E}$, 
 namely
$\mathcal{E}$ \emph{with dynamic topology} (denoted \evold{}) 
and $\mathcal{E}$ \emph{with static topology} (denoted \evols{}).
Here, ``dynamic'' refers to the ability of
creating and deleting new adaptable processes, something allowed in languages in \evold{} 
but not in those in \evols{}.
The definition of  $\evold{}$ and $\evols{}$ is
parametric on update patterns
%(contexts), denoted
$U_{}$.
%\todo{Careful, till now update patterns have been called contexts, this term appear in the introduction and till page 19, then context is alway used. I have added just the term context to link both terms, maybe you have a better solution}

% and $U_{s}$, respectively. Concrete instances for $U_{d}$ and $U_{s}$ will be discussed later on.

%More formally, we have the following definitions.

% We shall use 
% %Then, we introduce the calculi 
% \evold{1}--\evold{3}, \evols{1}--\evols{3} 
% to denote each of the six specializations of Evolvable CCS, in their dynamic and static variants.


%\todo{ subito dopo la submission a concur Gigio e Mario hanno fatto delle modifiche a questa sezione, Vi ricordate dove? adesso che risottomettiamo sono da chiarire meglio quei punti/ mettendoli piu' espliciti? }

%We will define terms of our calculi by means of syntactical definitions which make use of syntactical categories which can be process categories, e.g. $P$, or just auxiliary syntactical categories, e.g. $\pi$ used to define prefixes.



\begin{definition}[Dynamic $\mathcal{E}$ -- \evold{}]\label{d:finiteccs}
The class of $\mathcal{E}$ processes with dynamic topology (\evold{}) is described by the following
grammar: %, where $P$ is the only process category and it is the initial syntactical category: % which is an extension of CCS:
%\todo{Jorge: We can remove $\nil$ below, right?}
$$
P        ::= \component{a}{P} \sepr
          P \parallel P  \sepr ! \pi.P \sepr \sum_{i \in I} \pi_i.P_i  \qquad \quad  \pi   ::=  a \sepr \outC{a} \sepr \update{a}{U} 
$$
where $U::=P_{\bullet}$, as in Definition \ref{d:contexts}.
%\todo{add that the syntax of $U$ is obtained using Def \ref{d:contexts} on $P$}
\end{definition}

The definition of 
\evols{}
%evolvable CCS with static topology 
makes
use of two distinct process categories: $P$ and $A$.
Intuitively, $P$ correspond to processes defining the (static) topology of adaptable processes; these are populated by
terms $A$, which do not include subprocesses of the kind $\component{a}{Q}$.

\begin{definition}[Static $\mathcal{E}$ -- \evols{}]\label{d:eccsstatic}
The class of $\mathcal{E}$  processes with static topology (\evols{}) is described by the following
grammar: %, where $P$ and $A$ are the only process categories and $P$ is the initial syntactical category: % which is an extension of CCS:
$$
\begin{array}{lcl}
P       & ::=& \component{a}{P} \sepr
          P \parallel P \sepr A \\ %! \pi.A \sepr \sum_{i \in I} \pi_i.A_i  \\
A       & ::=&  A \parallel A \sepr
          ! \pi.A \sepr \sum_{i \in I} \pi_i.A_i \qquad
\pi  ::=  a \sepr \outC{a} \sepr \update{a}{\component{a}{U} \parallel A}
\end{array}
$$ 
where the syntax $U::=P_{\bullet}$, as in Definition \ref{d:contexts}, considering both $P$ and $A$ as process categories. %with process categories $P$ and $A$.
%where for every process $P \in  \evols{}$ that contains a subprocess  
%$\component{a}{Q}$, the following holds: for any $Q'$ and $U_{s}$,  
%if $\component{b}{Q'}$ occurs in $Q$
%then $\update{a}{\component{a}{U_s}}$ does not occur in $P$.
\end{definition}

Definition \ref{d:eccsstatic} relies on syntactic restrictions  to ensure that 
the nesting structure of adaptable processes in \evols{}  remains invariant.
The first restriction (i.e., no adaptable process is removed) is manifest in update prefixes, which are always of the form $\component{a}{U} \parallel A$; 
this forces the recreation of the adaptable process $a$ after every update, thus maintaining  the static structure of adaptable processes %the number of adaptable processes 
invariant.
%since the structure of adaptable processes must be preserved we require that the outermost process at $a$ is recreated.  
For the same reason, 
holes can only occur inside the recreated adaptable process: this way, 
processes cannot be relocated outside $\component{a}{U}$.
%whenever an update $\update{a}{P}$ occurs, the component is immediately recreated. 
The second restriction (i.e., no adaptable process is created) appears in the definition of $A$, 
which decrees that no new adaptable processes occur behind a prefix.
%Hence, components are preserved after update actions.
%The second restriction is more subtle
%as we have to ensure that only components that do not contain subcomponents can %be updated. 
%This is the purpose of the last part of the definition, which concerns 
%the subcomponents that could disappear after an update action.
As we will discuss below, the
operational semantics 
%for update actions 
ensures that these syntactic restrictions  %hold
are preserved along process execution.

\begin{remark}\label{rem:stdyn}
Observe that 
%evolvable CCS with static topology is a subcalculus of evolvable CCS, i.e. 
every \evols{} process is, from a syntactic point of view,
also an \evold{} process.
In fact, the 
%dynamic case updates always include the case 
update pattern 
$U = a[U'] \parallel A$
is a particular case of the possible update patterns  for \evold{} processes.
The correspondence between processes in \evols{}
and \evold{} from the point of view of their operational
semantics will be made more precise by Lemma \ref{lem:statvsdyn}.
%Moreover, because of the definition of \evols{},
%whenever an update $\update{a}{P}$ occurs, the component is immediately recreated. Hence, in \evols{} localities are never deleted.
\end{remark}


\paragraph{A Behavioral Characterization of Update}

We now move on to consider 
three concrete instances of 
update patterns $U$
and their associated 
variants of $\evold{}$ and $\evols{}$. 



%The variants of of \evold{} and \evols{} that adopt the general update pattern are denoted as \evold{1} and \evols{1}, respectively. 
%
%Ma $\evold{}$ and $\evols{}$ cosa erano????? Insiemi di termini??

%specialize the definition of Evolvable CCS (with dynamic or static topology) by defining 
%the grammar of the context $U$.
\begin{definition}[Update Patterns]\label{def:varianti}
%\quad \newline
We shall consider the following three instances of update patterns for \evols{} and \evold{}:
\begin{enumerate}
\item {\bf Full $\mathcal{E}$ (\evold{1} and \evols{1}).}
The first 
update pattern
%variant 
admits all kinds of contexts for update prefixes, i.e., $U ::= P_{\bullet}$.
%\begin{eqnarray*}
%U & ::= & \sum_{i \in I} \pi_i.U_i  \sepr \component{a}{U}  \sepr
%          U \parallel U  \sepr ! \pi.U \sepr \bullet \\
%\end{eqnarray*}
These variants, corresponding to the above \evold{} and \evols{},
are denoted also with \evold{1} and \evols{1}, respectively. 
%Notice that, in accordance with the static topology of \evols{} processes,  $U_s$ admits all kinds of contexts that do not include components.


% In the case of evolvable CCS with dynamic topology,
% the first specialization admits for $U$ all kinds of contexts.
% 
% $$
% U \ ::= \ \sum_{i \in I} \alpha_i.U_i  \sepr \component{a}{U}  \sepr
%           U \parallel U  \sepr ! \alpha.U \sepr \bullet
% $$
% 
% Analogously, %Similarly, 
% for evolvable CCS with static topology,
% we admit for $U$ all kinds of contexts that do not include components.
% 
% $$
% U \ ::= \ \sum_{i \in I} \alpha_i.U_i  \sepr
%           U \parallel U  \sepr ! \alpha.U \sepr \bullet
% $$

\item {\bf Unguarded $\mathcal{E}$ (\evold{2} and \evols{2}).}
In the second
update pattern, 
%variant, 
holes cannot occur in the scope of prefixes in $U$:
%$ \qquad
$$
U  ::=  P \sepr \component{a}{U}  \sepr    U \parallel U  \sepr \bullet  %$
$$
The variants of \evold{} and \evols{} that adopt this update pattern are denoted
\evold{2} and \evols{2}, respectively. 
%while $U_s$ leads to \evols{2}.
%Notice that $U_s$ is as $U_d$ in which components are excluded and $A$ is used instead of $P$.





\item {\bf Preserving $\mathcal{E}$ (\evold{3} and \evols{3}).}
In the third update pattern, the 
%In this case, the 
current state of the adaptable process is always preserved.
Hence,  
it is only possible to add new adaptable processes and/or behaviors in parallel or to relocate it:
%\begin{eqnarray*}
%$ \qquad
$$
U  ::=  \component{a}{U}  \sepr U \parallel P \sepr \bullet
$$

%\end{eqnarray*}
The variants of \evold{} and \evols{} that adopt this update pattern are denoted 
\evold{3} and \evols{3}, respectively. 


\end{enumerate}

 
\end{definition}


%\paragraph{Semantics.~} 
\subsection{Semantics} 

The semantics of \evol{} processes is given in terms of a 
Labeled Transition System (LTS). 
We  introduce some auxiliary definitions first.

\begin{definition}\label{d:srtcong}
\emph{Structural congruence} is  the smallest
congruence relation generated by the following laws: 
$P \parallel Q \equiv Q \parallel P$; $P \parallel (Q \parallel R) \equiv (P \parallel Q) \parallel R$.
\end{definition}

\begin{definition}[Normal Form]\label{d:nform}
An \evol{} process $P$ is said to be in \emph{normal form} iff
%$$P \equiv \prod_{i=1}^{l} P_i \parallel \prod_{j=1}^{m}\prod_{k=1}^{n_j} \component{a_j}{P'_{j,k}} $$
$$P = \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}} $$
  where, for $i \in \{1,\ldots,m\}$, $P_i$ is not in the form $Q \parallel Q'$ or $a[Q]$, 
  and, for all $j \in \{1,\ldots,n\}$,  %${P'_{j,k}}$ 
${P'_{j}}$ is in normal form.
Note that if $m = 0$ then 
the normal form is simply 
$P = \prod_{j=1}^{n} \component{a_j}{P'_{j}}$; similarly, if $n=0$ then the normal form is $P = \prod_{i=1}^{m} P_i$.

\end{definition}

%Every process can be rewritten in normal form up-to structural congruence, as stated in the following lemma.

 \begin{lemma}\label{lem:normalform}
 Every \evol{} process
% $P \in \evol{}$ %we have that $P$ 
 is structurally congruent
  to a process in normal form.%, i.e. 
%$$P \equiv \prod_{i=1}^{l} P_i \parallel \prod_{j=1}^{m}\prod_{k=1}^{n_j} \component{a_j}{P'_{j,k}} $$
%$$P \equiv \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}} $$
 % where $P_i$ is not in the form $Q \parallel Q'$ or $a[Q]$
  %and %${P'_{j,k}}$ 
%${P'_{j}}$ is in normal form.
 \end{lemma}
 
We now define the \emph{containment structure denotation} of a process.
Intuitively, it captures the tree-like structure induced by the nesting of adaptable processes.

% : intuitively the depth of a tree is given by the depth of the nesting of components. 
 %See Figure \ref{fig:proc2tree} for an example.

%\begin{figure}[t]
%\input{tree}
 %\caption{The tree denotation of the process $a.P \parallel \update{b}{Q} \parallel \component{b}{c.R \parallel \component{d}{e.S}}  \parallel \component{f}{g.T}$}\label{fig:proc2tree}
%\end{figure}

 \begin{definition}[Containment Structure]\label{def:cstr}
  Let $P = \prod_{i=1}^{m} P_i \parallel \prod_{j=1}^{n} \component{a_j}{P'_{j}}$ be an \evol{} process in normal form.
The \emph{containment structure denotation} of $P$, denoted $\CStr(P)$,  is built as follows. 
  The root is labeled $\epsilon$, and has $n$ children: 
   the subtrees recursively built from processes $P'_{1}, \dots, P'_{n}$ 
   with roots labeled $a_1, \dots, a_n$ (instead of $\epsilon$), respectively.
%      respectively, where the only difference is that the roots are labeled $a_1, \dots, a_n$.
%\todo{Mario suggests to move the word ``respectively'' above to the end of the sentence, to me it is better where it is, i would ignore his comment}
%When $n=0$, we say that $\CStr(P) = \epsilon$ is the \emph{empty} containment structure denotation.
When $n=1$, we say that the containment structure
$\CStr(P)$ is \emph{single-child}.
\end{definition}
 \begin{example}\label{ex:cstr}
 Consider the processes $P$, $Q$, and $R$ defined as 
 $$
 P = P_{1} \parallel \component{b}{P_{2}} \parallel \component{a}{P_{3} \parallel \component{c}{S}}
 \qquad
 Q =  a.P_{2} \parallel \component{b}{P_{3}} \parallel \component{a}{\component{c}{S}}
 \qquad R = P_{1} \parallel \component{d}{S}
 $$ where 
 $P_{1}, P_{2}, P_{3}$ do not contain adaptable processes.
 Then, $P$ and $Q$ have the same 
 containment structure denotation; it is depicted in 
 Figure \ref{f:csd} (left). 
 As for $R$, the
 containment structure denotation $\CStr(R)$, that is single-child,
is depicted in Figure \ref{f:csd} (right).
 \begin{figure}[t]
 \linefigure
 \begin{center}
\rowheight=1.0pc
\xytree{
       & \xynode[-1,1]{$\epsilon$} \\
       \xyterminal{$b$} & & \xynode[0]{$a$} \\
       & & \xytrinode{$c$}\\
       & & \xyterminal{$\CStr(S)$} 
}
\qquad \qquad
\xytree{
        \xynode[0]{$\epsilon$} \\
        \xytrinode{$d$}\\
        \xyterminal{$\CStr(S)$} 
}
\end{center}
\caption{Containment structure denotation for $P =  P_{1} \parallel \component{b}{P_{2}} \parallel \component{a}{P_{3} \parallel \component{c}{S}}$ and $R = P_{1} \parallel \component{d}{S}$, as in Example \ref{ex:cstr}.} \label{f:csd}
 \linefigure
 \end{figure}
  \end{example}
 
 Given an update pattern $U$, 
the following two definitions on 
%static processes 
\evols{} processes
indicate the number of holes 
and adaptable processes 
which syntactically occur in $U$, 
respectively.
In both cases, we do not consider occurrences inside nested update prefixes.
 
  
%\begin{definition}
%Let $P$ be an \evols{} process.
%The number of adaptable processes which occur at top level in $Q$, denoted
%\numtap{U}, is inductively defined as follows:
%\begin{align*}
%\numtap{\component{a}{P}} &= 1 & \numtap{P_{1} \parallel P_{2}}  &=  \numtap{P_{1}} + \numtap{P_{2}} \\
% \numtap{\sum_{i \in I}\pi_{i}.P_{i}} & =  0 & \numtap{! \pi.P} & =0 
%\end{align*}
%\end{definition}

 \begin{definition}\label{d:numap}
Let $U$ denote an \evols{}  update pattern or an \evols{}  process.
The number of adaptable processes which occur in $U$, denoted
\numap{U}, is inductively defined as follows:
\begin{align*}
\numap{\bullet} & = 0 & \numap{U_{1} \parallel U_{2}} & =  \numap{U_{1}} + \numap{U_{2}} &  \numap{! \pi.U} &= 0 \\
\numap{\component{a}{U}} &= 1 + \numap{U} & \numap{\sum_{i \in I}\pi_{i}.U_{i}} &= 0\, 
\end{align*}

%$num_{c}(U)$ denotes the number of adaptable processes which syntactically occur in $U$, not inside update prefixes. 
\end{definition}


Notice that in the above definition, as we are considering \evols{}  processes, the number of adaptable processes after a prefix is necessarily 0.



\begin{definition}
Let $U$ be an \evols{}  update pattern.
The number of holes which occur in $U$, denoted
\numholes{U}, is inductively defined as follows:
\begin{align*}
\numholes{\bullet} & = 1 & \numholes{U_{1} \parallel U_{2}} & =  \numholes{U_{1}} + \numholes{U_{2}} &  \numholes{! \pi.U} &= \numholes{U}\\
\numholes{\component{a}{U}} &= \numholes{U} &
\numholes{\sum_{i \in I}\pi_{i}.U_{i}} &= \sum_{i \in I}\numholes{U_{i}\,}  & &
 \end{align*}
\end{definition}

 The following auxiliary notation will be useful to formalize the properties of  $\evols{}$ processes along reductions.

\begin{definition}
Let $U$ be an \evols{} update pattern. The number of prefixed holes occurring in $U$, denoted
\numph{U}, is inductively defined as follows:
\begin{align*}
\numph{\bullet} &= 0 & \numph{\component{a}{U}} &= \numph{U} & \numph{U_{1} \parallel U_{2}}  &=  \numph{U_{1}} + \numph{U_{2}} \\
 \numph{\sum_{i \in I}\pi_{i}.U_{i}} & =   \sum_{i \in I}\numholes{U_{i}} & \numph{! \pi.U} & =\numholes{U}
\end{align*}
%\todo{Replaced $\numpha{\cdot}$ with $\numholes{\cdot}$}
%where the auxiliary measure $\numpha{U}$ is inductively defined as 
%\begin{align*}
%\numpha{\bullet} &= 1  & \numpha{U_{1} \parallel U_{2}}  &=  \numpha{U_{1}} + \numpha{U_{2}} \\
% \numpha{! \pi.U}  & =\numpha{U} & \numpha{\sum_{i \in I}\pi_{i}.U_{i}}  & =  \sum_{i \in I}\numpha{U_{i}} 
%\end{align*}
\end{definition}


\begin{example}
Let $P$ and $U$ be an \evols{} process and an \evols{} update pattern  defined as 
$$
P = 
\componentbbig{a}{\component{b}{Q_{1}} \parallel P_{1}} \parallel
\updatebig{a}{U}.P_{2} 
\qquad 
U = \outC{b}.\update{d}{\bullet \parallel U_{1}}.\nil \parallel \component{b}{a.\bullet \parallel \bullet}
$$
Then we have: 
\begin{itemize}
\item $\numap{P} = 2 + \numap{Q_{1}} + \numap{P_{1}}  + 0$ and $\numap{U} = 1$
%\item $\numholes{P} = \numholes{R_{2}} + \numholes{Q_{1}} + \numholes{Q_{2}}$ and 
\item $\numholes{U} = 2$ and  $\numph{U} = 1$.
%\item $\numph{P} = \numph{R_{2}} + \numph{Q_{1}} + \numph{Q_{2}} $
\end{itemize}
\end{example}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We are now ready to define an LTS semantics for \evols{} and another one for \evold{}.
Both LTSs are generated by the set of rules in Figure \ref{fig:ltswithalpha}; they 
only differ on a condition associated to update actions.
This is the content of the following definition.

\begin{definition}[LTS for $\evold{}$ and $\evols{}$]\label{d:lts}
Given transition labels 
\[
\alpha    ::=  ~~ a \sepr \outC{a} \sepr \component{a}{P} \sepr \update{a}{U} \sepr \tau
\]
the LTS for \evold{}, denoted $\arro{~\alpha~}_{d}$,  
is defined by the rules in Figure \ref{fig:ltswithalpha} in which, in rules \rulename{Tau3} and \rulename{Tau4},
we decree $\mathsf{cond}(U,Q){=}\mathtt{true}$. 

Similarly, 
the LTS for \evols{}, denoted $\arro{~\alpha~}_{s}$,  
is defined by the rules in Figure \ref{fig:ltswithalpha} in which,
 in rules \rulename{Tau3} and \rulename{Tau4},
  we decree that $\mathsf{cond}(U,Q)$ holds if %, for any $A$ as in Definition \ref{d:eccsstatic}, 
we have:
  \begin{enumerate}
  \item $\CStr(\component{a}{Q}) = \CStr(\component{a}{\fillcon{U'}{Q}} \parallel A)$  where $U=\component{a}{U'}\parallel A$, for some $U', A$,  and 
  %\item $\CStr(\component{a}{Q}) = \CStr(\component{a}{\fillcon{U'}{Q}} \parallel A)$ \add{where $U=\component{a}{U'}\parallel A$}, and 
  \item $\numph{U} > 0 \Rightarrow \numap{Q} = 0$.
  \end{enumerate}
%\todo{it is not necessary to say what A is, it is implicit when you define U}
\end{definition}

\begin{remark}\label{r:fbranch}
The LTS for \evols{} and \evold{} are finitely branching. 
The proof proceeds by induction on the syntactic structure of terms; the base cases are $\sum_{i\in I}\pi_i.U_i$ and $!\pi.U$.
\end{remark}
%\todo{Add type-inspired justification for the second part of the condition: the intention is to ensure that behind a process you have a process from $A$, which doesn't have components. Use this counterexample, by Mario: 
%$\component{b}{\component{a}{\nil}} \parallel \update{b}{\component{b}{\component{a}{b.\bullet}}}$}


\begin{figure}[t]
\linefigure
$$
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}
\qquad 
%  \mathrm{\textsc{Upd}}~~~\update{a}{P_1}.P_2 \arro{\update{a}{P_1}}  P_2
%$$
%$$
\inferrule[\rulename{Sum}]{}{\sum_{i\in I} \pi_i.P_i \arro{~\pi_j~}  P_j  ~~(j \in I)}  
%\rightinfer	[\textsc{Rec}]
 %			{rec \,X.P \arro{\alpha} P}
 %			{P\sub{rec \, X.P}{X} \arro{\alpha} P'}
 %\quad
\qquad
\inferrule[\textsc{(Repl)}]{}{!\pi.P \arro{~\pi~}  P \parallel !\pi.P }
$$
$$
\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}
\quad 
\inferrule[\rulename{Act1}]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}			
\quad
\inferrule[\rulename{Tau1}]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}
$$
$$
\inferrule[\rulename{Tau3}]{P_1 \arro{~\component{a}{Q}~} P_1'\andalso P_2 \arro{~\update{a}{U}~} P_2'  \andalso \mathsf{cond}(U,Q)}{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{U}{Q}  }{\star} \parallel P_2'}
$$

\caption{LTS for \evols{} and \evold{}.
Rules \rulename{Act2}, \rulename{Tau2}, and \rulename{Tau4}---the symmetric counterparts of 
\rulename{Act1}, \rulename{Tau1}, and \rulename{Tau3}---have been omitted.} \label{fig:ltswithalpha}
%\end{table}
\linefigure
\end{figure}

We give intuitions on  both LTSs.
%There are five kinds of actions; we use $\alpha$ to range over them. 
In addition to the standard CCS actions (input, output, $\tau$), we consider two
complementary actions for process update: 
$\update{a}{U}$ and $\component{a}{P}$.
The former represents the availability of an update pattern $U$ for the adaptable process at $a$;
the latter expresses the fact that the adaptable process at $a$, with current state $P$, is ready to update. %being part of an update operation.
We often write $\arro{~\alpha~}$ instead of $\arro{~\alpha~}_{d}$ and $\arro{~\alpha~}_{s}$; 
the actual LTS used in each case will be clear from the context.
Similarly, we define $\arro{~~~}$ as $\arro{~\tau~}$.

In Figure \ref{fig:ltswithalpha}, 
%, which are common to both  $\pired_{d}$ and $\pired_{s}$.
%Intuitions for some rules of the LTS follow.
rule \rulename{Comp} represents the contribution of a process at $a$ in an update operation; 
we use  $\star$ to denote a unique placeholder. 
%\todo{This placeholder should be unique and different from every name in $\mathcal{N}$. Probably there should be one placeholder for each component, so as to keep updates consistent...JP}
Rule \rulename{Loc}
formalizes
transparency of localities.
%The only point in which the LTS of \evold{}
%and that of \evols{} differ is in 
%condition $\mathsf{cond}(U,Q)$, associated to 
Rules \rulename{Sum}, \rulename{Repl}, 
\rulename{Act1},
and \rulename{Tau1} 
 are standard.
 Rule \rulename{Tau3} formalizes process evolvability.
To realize the 
evolution of an adaptable process at $a$, it requires: 
%can be explained as follows.
%The update action offers a process $U$ for updating the process at $a$ which, by virtue of rule \rulename{Comp}, is 
%represented in $P'_{1}$ by $\star$.
%Process $Q$---the current state of $a$--- is then used to fill the holes in $U$.
%Provided that $\mathsf{cond}(U,Q)$ holds, 
%the update action is completed by replacing all occurrences of $\star$ in $P'_{1}$ with process $\fillcon{U}{Q}$.
(i)  a process $Q$---which represents its current state; 
(ii) an update action offering an update pattern  $U$ for updating the process at $a$---which is represented in $P'_{1}$ by $\star$ (cf. rule \rulename{Comp});
(iii) that $\mathsf{cond}(U,Q)$ holds (cf. Definition \ref{d:lts}).
As a result, %every occurrence of 
$\star$ in $P'_{1}$ is replaced with process $\fillcon{U}{Q}$ (cf. Definition \ref{d:fillit}).
%This way, rule \rulename{Tau3} is the only point in which the LTS of \evold{} and that of \evols{} differ.
 
It is useful to elaborate on the definition of $\mathsf{cond}(U,Q)$---the only point in which the LTS of \evold{} and that of \evols{} differ.
%which arises in rules \rulename{Tau3} and \rulename{Tau4}, in the update of an adaptable process with current state $Q$ according to the update pattern $U$.
While 
$\mathsf{cond}(U,Q)$  does not have influence on the update actions of 
\evold{} processes, it does ensure that the syntactic restrictions associated to \evols{} processes are preserved along transitions. 
As specified in Definition \ref{d:lts}, 
the condition 
for \evols{} processes 
is given in two parts.
The first part ensures that the current structure of nested adaptable processes---the containment structure denotation from $\component{a}{Q}$---is preserved once $Q$ is substituted into $U$ as a result of the transition.
The second part of the condition ensures that no new adaptable processes will appear behind prefixes as a result of 
the update operation. 
Recall that by the syntactic restrictions enforced by 
Definition \ref{d:eccsstatic}, adaptable processes cannot occur behind prefixes.
In fact, and  using the terminology introduced in that definition, 
the syntax of \evols{}  decrees that only processes in process category $A$ (which do not contain adaptable processes)
can occur behind prefixes.
The second part of the condition ensures precisely this.  
As a simple example, 
this  part of the condition rules out the synchronization of 
adaptable process $\component{b}{\component{a}{\nil}}$
with  update prefix
$\update{b}{\component{b}{\component{a}{b.\bullet}}}.Q$,
as 
it would lead to the non static process 
$\component{b}{\component{a}{b.\component{a}{\nil}}} \parallel Q$.

By considering the syntactic restrictions associated to \evols{} processes,
the following lemma characterizes  the conditions under which $\mathsf{cond}(U_{0},Q)$ holds for them.

%It is useful to  characterize precisely the conditions under which $\mathsf{cond}(U,Q)$ holds for \evols{} processes.
%This is the content of the following lemma \add{where considering the syntactic restrictions associated to \evols{} processes, we characterize $\mathsf{cond}(U,Q)$.}



%\todo{here there was a tiny detail as in def 2.15, basically U is the whole process inside the update while U' is only the part with the bullet, so Mario removed the name from the lemma and added the description to the previous text} 

\begin{lemma}%[Characterization of $\mathsf{cond}(U,Q)$]
\label{lem:statvsdyn}
Let $Q$ and $U_{0} = \component{a}{U} \parallel A$   be an $\evols{}$ process and an $\evols{}$ update pattern, respectively. Also, let $A$ be as in Definition \ref{d:eccsstatic}. We have
\begin{equation}
\CStr(\component{a}{Q}) = \CStr(\component{a}{\fillcon{U}{Q}} \parallel A) \land  (\numph{U} > 0 \Rightarrow \numap{Q} = 0)\label{eq:st}
\end{equation}
if and only if one of the following holds:
\begin{enumerate}
  \setcounter{enumi}{-1}
\item $\numholes{U}=0 \wedge \CStr(Q) = \CStr(U)$.
\item $\numholes{U}=1  \wedge \numap{U} = 0 \wedge (\numph{U} > 0 \Rightarrow \numap{Q} = 0)$ 
\item $\numholes{U}>1 \wedge \numap{U} = 0\wedge \numap{Q} = 0$.
\end{enumerate}
\end{lemma}
\begin{proof}[Proof]
%\todo{Check and adjust the text below}
The ``if'' direction is straightforward by observing that
by definition $\numap{A}=0$.
Therefore, 
(\ref{eq:st}) reduces to 
$$\CStr(Q) = \CStr(\fillcon{U}{Q}) \land  (\numph{U} > 0 \Rightarrow \numap{Q} = 0)$$
and the analysis focuses on the structure of $U$. Hence if $\numholes{U}=0$ then immediately from (\ref{eq:st}) we have $\CStr(Q) = \CStr(U)$.
If $\numholes{U}=1$ then as  $\CStr(Q) = \CStr(\fillcon{U}{Q})$ we have that $\numap{U} = 0$ and from the second part of (\ref{eq:st}) we conclude $(\numph{U} > 0 \Rightarrow \numap{Q} = 0)$.
Finally, if $\numholes{U}>1$ following from   $\CStr(Q) = \CStr(\fillcon{U}{Q})$ we conclude $\numap{U} = 0$ and $\numap{Q} = 0$.
%It is easy to check that the three items cover every possible case for hole occurrences in $U$ 
%(no holes, exactly one hole, more than one hole) and that the second part of (\ref{eq:st})
%is only applicable when $\numholes{U}=1$. 

As for the "only if" direction, we consider each item separately:
\begin{itemize}
\item Item 0.:  
Then $Q$ occurs exactly once only at the left-hand side of the desired equality.
Using the first part of the item (i.e., $\numholes{U}=0$) we infer that  $\fillcon{U}{Q} = U$.
Since by definition $\numap{A}=0$, we have that 
the second part of the item (i.e., $\CStr(Q) = \CStr(U)$) is enough to obtain
$\CStr(\component{a}{Q}) = \CStr(\component{a}{U} \parallel A)$, as wanted.

\item Item 1.: Then $Q$ occurs exactly once in both sides of the desired equality. 
The second part of the item (i.e., $\numap{U} = 0 $) guarantees that 
$\fillcon{U}{Q}$ does not involve any adaptable processes different from those in $Q$.
The third condition ensures that no adaptable processes occur behind prefixes: 
if $Q$ has adaptable processes then it should necessarily occur at the top level in $\fillcon{U}{Q}$.
Hence, the thesis follows.

\item Item 2.: Then $Q$ occurs exactly once in the right-hand side of the equality, and arbitrarily many times in the left-hand side.
The second part of the condition, on the number of adaptable processes in $U$, follows the same motivations as in the previous case.
Given the possibility of arbitrarily many occurrences of $Q$ in the left-hand side, 
the only option 
to ensure identical containment structure denotations in both sides
is to forbid adaptable processes inside $Q$, hence the third part of the condition.
\end{itemize}
\end{proof}

%Consequently, we have the following lemmas:

The following lemma is standard:
\begin{lemma}
Let $P$ be an \evol{} process.
Structural congruence is preserved by reduction: 
if $P \equiv Q$ and $P \pired P'$, then also $Q \pired Q'$ for some $P' \equiv Q'$.
\end{lemma}

The following lemma states that \evols{} processes are closed under reduction.
Hence, the operational semantics of \evols{} preserves the syntactic conditions of Definition \ref{d:eccsstatic}.

% \input{evolsclosure}
 \begin{lemma}[Static topologies are preserved by reduction]\label{l:esred}
 Let $P$ be an \evols{} process.
 If $P \pired P'$ then
 also $P'$ is an  \evols{} process. Moreover, $\CStr(P)=\CStr(P')$.
 %, thus adhering to the syntactic restriction imposed by Definition~\ref{d:eccsstatic}. 
 %In particular, if the transition involves the update of a component 
 %(i.e., a $\tau$-transition obtained using rules $\textsc{Tau3}$/$\textsc{Tau4}$), 
 %%the assumption given after 
 %Definition~\ref{d:eccsstatic} guarantees
 %that a term belonging to the syntactic category $A$
 %is used in place of  $\bullet$, and hence 
 %$P'$ respects the syntax of \evols{} processes.
 \end{lemma}
 
 \begin{proof}
 By induction on the derivation of $P \arro{~\tau~} P'$.
 See \ref{ap:esred}, page \pageref{ap:esred}.
 \end{proof}

\newcommand{\proj}[2]{\ensuremath{#1\downarrow#2}}


\subsection{From Static to Dynamic Topologies}\label{ss:stdyn}
%$S$ is a set of pairs component names, component structures
%
%l'idea e' che prima guardo staticamente la component structure interna ai componenti poi quando c'e' un'azione che si sincronizza lo trasformo in base a quello, quindi ho un prefisso di update e memorizzo nel tipo la struttura dei
%possibili matchanti in modo da esser sicuro che faccia match: il match si stabilisce su tutta la struttura!
%Quindi nella struttura ho gia' il nome del componente!
%
%quindi ho una funzione che dato un termine mi torna l'insieme delle strutture
%di tutti i componenti in esso.
We have already remarked that from a syntactic
point of view every \evols{} process is also an \evold{} process.
As far as the operational semantics is concerned, 
an \evols{} process could have less possible computations
due to the additional constraint $\mathsf{cond}(U,Q)$ 
of the rules \rulename{Tau3} and \rulename{Tau4}. Nevertheless, 
in this section we show that it is always possible to translate 
a process with static topology into a 
process with dynamic topology which has the same 
semantics (the two LTSs are isomorphic). More precisely, we will
define an encoding 
$\dyn{\cdot}: \evols{} \to \evold{} $
%$\dyn{P}$ that translates  a static process $P$ into an equivalent dynamic process
such that the following holds: 
$$P \pired_s P'\text{ if and only if }\dyn{P} \pired_d \dyns{P'}{S}$$

%We now discuss and formalize the conditions under which an \evols{} process can be transformed into an equivalent \evold{} process.
%More precisely, we are interested in the class of $\evols{}$ processes 
%whose semantics does not change when considered as a dynamic process:  %that behaves accordingly to the semantics of $\evold{}$:
%the class of \evols{} processes for which 
%$\mathsf{cond}(U,Q)$ always holds.
%Establishing such a relation between \evols{} and \evold{} processes 
%will be useful to transfer (un)decidability results.
%We need some auxiliary definitions.

We start by presenting some auxiliary definitions.
\begin{definition}\label{d:cstrs}
Let $P$ be an \evols{} process.
We define the set
$$\CStrs(P) = \{ \CStr(a[P']) \mid a[P'] \text{ is a subterm of } P \}$$ %, where $subt$ is the subterm relation. 
%\todo{Just before, do we need to add `` for some $a,P'$'' ? This is suggested by Rev 3-12, ESOP}
\end{definition}

Hence, $\CStrs(P)$ is a set of trees: 
it contains the 
%containment structure denotation of $P$ 
%(which is defined as a tree, see Definition \ref{def:cstr}), 
%as well as all the 
containment structure denotations of  the adaptable processes occurring in  $P$. 
Notice that by construction $\CStrs(P)$ is a set of single-child containment structure denotations.

\begin{example}
Let $P$ be as  in Example \ref{ex:cstr}. 
Then, we have $$\CStrs(P) = \{\CStr(\component{a}{P_{3} \parallel \component{c}{S}}), \CStr(\component{b}{P_{2}}), \CStr(\component{c}{S})\} \cup \CStrs(S)$$
\end{example}



%%We have already remarked the fact that every process in  $\evols{}$ is also a process in $\evold{}$ (cf. Remark \ref{rem:stdyn}).
%We are interested in the class of $\evols{}$ processes that behaves accordingly to the semantics of $\evold{}$.
%That is to say, \evols{} processes for which the conditions 
%implied by 
%$\mathsf{cond}(U,Q)$ % = \CStr(a[Q]) = \CStr(\fillcon{U}{Q})$ 
%%\todo{and the second part of the condition} 
%in Definition \ref{d:lts}
%always hold.
%The following lemma characterizes such ``well-behaved'' static processes.


  

%\todo{meglio un lemma o un remark?}
%\begin{remark}
%Using Lemma \ref{lem:statvsdyn} 
%it is possible to show that the class of \evols{} processes that do not contain nested adaptable processes 
%(i.e., ``flat'' processes) behaves as processes in \evold{}.
%\end{remark}

%Based on Lemma \ref{lem:statvsdyn}, 
%it is possible in general to encode an \evols{}  process into an \evold{}  process that preserves its behavior.
%This is the purpose of the encoding 
%$\dyn{\cdot}: \evols{}~\to~\evold{}$, which we define now. 
%First, we need some notation. 

\begin{mynotation}\label{not:enc} Below $P$ and $a$ stand for an \evols{} process and a name, respectively.
\begin{itemize}
\item Let $S$ be   
a set of %single-child 
containment structure denotations. We write $\proj{S}{a}$  
 to represent the %(possibly empty) 
 subset of single-child containment structure denotations of $S$ in which the label of the only child of the root is $a$. 
% \todo{ho cambiato il nome da g a $\varphi$, g poteva essere confuso con un nome di canale}

\item We assume an injective function $\varphi$ 
 that associates
%that maps every 
containment structure denotations
%$\CStr(a[P])$  %(cf. Definition \ref{def:cstr})
to 
names in $\mathcal{N}$.
We use $\kappa,\kappa',\ldots$ to range over the codomain of  $\varphi$.
Moreover, 
for every $P$ such that $\numap{P}= 0$,  we fix $\ecs{\CStr(\component{a}{P})} = \kappa_{a}$.
%Hence, $a \neq b$ implies $\kappa_{a} \neq \kappa_{b}$, for any $a, b$.
The definition of $\varphi$ extends to sets of containment structure denotations as expected; 
 this way, e.g., $\ecs{\proj{S}{a}}$ stands for the set of names associated to those single-child
 containment structure denotations in $S$ with label $a$. 
  With a slight abuse of notation, we sometimes write $\ecs{\component{a}{P}}$ instead
 of $\ecs{\CStr(\component{a}{P})}$.
 %single-child 
%Given a static process $P$, such an encoding relates the containment structure of $P$  with a single name in \evold{}.
% of a static process $P$ works on a sort of powerset construction where we add denotations
%In the following definition we consider single-child component structure denotations to be component structure denotations $\CStr(a[P])$ for some $a \in \mathcal{N}$ and $P \in \evols{}$. 
%In the definition below, w
%We use $\kappa, \kappa', \ldots$ to range over single-child containment structures.
%\todo{l'ultimo itemize e' stato messo dentro la tabella, a detta di Mario cosi' era moooolto piu' chiaro}
%\item We write $\xi \pi.P$ to denote a possibly replicated prefixed process, 
% that is, $\xi \pi.P$ denotes either $!\pi.P$ or $\pi.P$.
 \end{itemize}
\end{mynotation}
 
 We are now ready to present the definition of $\dyn{\cdot}$.
 
\begin{definition}%[NEW VERSION]
\label{def:din}
Adopting the notations in Convention \ref{not:enc}, 
let $P $ and $U$ be an \evols{} process and an \evols{} update pattern, respectively.
Also, let $S$ be a set of containment structure denotations such that $\CStrs(P) \subseteq S$. 
Moreover, assume $\mathrm{err} \notin \ecs{S}$. %a set of names $\mathcal{N}'$ such that $\mathcal{N} \cup \ecs{S} \cup \{\mathrm{err}\} \subseteq \mathcal{N}'$.
%We inductively define $\dyn{P}$ as an $\evold{}$ process over $\mathcal{N}'$, as in Figure \ref{f:encsd}.
The encoding of $P$ into an \evold{} process over $\mathcal{N}$, denoted $\dyn{P}$, 
is inductively defined in Figure \ref{f:encsd}, where
%\todo{Mario voleva togliere C1, ma poi la spiegazione viene un casino, io lo lascerei, gli scrivero' una mail quando torno}
\begin{itemize}
\item $C1$ stands for $\numholes{U}=0$; 
\item $C2$ stands for $(\numholes{U}=  1\wedge \numph{U} > 0 \land \numap{U} = 0) \lor (\numholes{U}> 1 \land \numap{U} = 0)$; 
\item $C3$ stands for $\numholes{U}= 1 \wedge \numph{U} = 0 \land \numap{U} = 0$; 
\item $C4$ stands for $\numholes{U} \neq 0 \wedge \numap{U} \neq 0$.
\end{itemize}
\end{definition}


We now comment on the definition in Figure \ref{f:encsd}.
Unsurprisingly, the encoding only concerns adaptable processes and update prefixes; input and output prefixes are not modified (cf. line $(6)$), 
 and guarded sum, parallel composition, and holes are treated homomorphically (cf. lines $(7)$, $(8)$, and $(9)$, respectively).
 Intuitively, the encoding 
 captures correct update actions by 
 renaming every adaptable process and update prefix according to their containment denotation structure.
 This way, an adaptable process  $\component{a}{P}$ 
 is translated into an adaptable process on name $\kappa$, 
 which depends on its containment structure denotation (cf. line $(1)$).
The intention of this renaming is to allow synchronization only with update prefixes on name $\kappa$, 
that is, with update prefixes having the same containment structure denotation; 
this way, condition $\CStr(U) = \CStr(Q)$ in the LTS of \evols{} is enforced via name equality.
As for the encoding of a process $P$ at $a$, it is important to observe that 
 the definition of \evols{} ensures that holes syntactically occurring in $P$ do not occur at top level---they can only appear inside an update prefix.
As such, they are handled by lines $(2)$--$(7)$ in recursive applications of the encoding.
%\add{Notice that $\bullet$ cannot occur in $\component{a}{P}$. This follows from the fact that the initial process on which the encoding is applied is an \evols{} process, moreover when the encoding is recursively applied  conditions $C1$--$C4$ ensures that $\bullet$ would not occur inside a component.}

Clearly, update prefixes must be modified accordingly; 
there are four different possibilities,  represented by conditions $C1$--$C4$ of Definition~\ref{def:din}:
%We explain these conditions separately:
\begin{itemize}
\item $C1$ captures the cases in which the update pattern $U$  does not contain holes, i.e., $U$ is a process. 
Update prefixes with update patterns of this kind are encoded homomorphically, renaming the prefix accordingly (cf. line $(2)$).
Together with the above explained renaming of adaptable processes with respect to  the structure of their contents, 
this condition corresponds to Lemma \ref{lem:statvsdyn}(0).


\item $C2$ captures the cases in which the update prefix is only meant to interact with adaptable processes whose content have no adaptable processes. 
As explained before, 
and by the definition of $\varphi$,
these are adaptable processes of the form $\component{\kappa_{a}}{P}$ (with $\numap{P}=0$); this explains the encoding described in line $(3)$.
According to Lemma \ref{lem:statvsdyn}, this is the case
when (i) 
the update pattern $U$ of the update prefix has exactly one hole that occurs behind a prefix (cf. Lemma \ref{lem:statvsdyn}(1) when $\numph{U} > 0$)
or (ii) $U$ has more than one hole (cf. Lemma \ref{lem:statvsdyn}(2)).


\item $C3$ captures the cases in which the update pattern $U$  has exactly one hole which does not occur behind a prefix.
These are update prefixes that may synchronize with any adaptable process at name $a$. 
In order to account for all the possibilities, 
each non replicated update prefix at $a$ is encoded as a sum of prefixed processes,
each summand corresponding to an update prefix on a name $\kappa_{i} \in \ecs{\proj{S}{a}}$. 
The only difference between the summands 
is the name of the update prefix; the update pattern within the update prefix and  its continuation is the same for all of them  (cf. line $(3a)$).
When the update prefix is replicated, rather than the sum  of all possible adaptable processes, 
we consider their product (cf. line $(3b)$).
This condition corresponds to Lemma \ref{lem:statvsdyn}(1) when $\numph{U} = 0$.

\item $C4$ captures those update patterns that do not adhere to any of the conditions of Lemma \ref{lem:statvsdyn}.
Hence, interaction with these prefixes may lead to ill-formed \evols{} processes. 
To prevent such undesirable interactions, these update prefixes are renamed into $\mathrm{err}$---a distinguished name signaling error  (cf. line $(5)$).

\end{itemize}


%% NEW VERSION OF THE DEFINITION
%\begin{figure}
%\begin{align*}
%(1)~& \dyn{\component{a}{P}} &= &~\componentbbig{\kappa}{\dyn{P}}  \quad\text{with $\kappa = \ecs{\CStr(\component{a}{P})}$} & \\
%(2)~& \dyn{\xi \, \update{a}{\component{a}{P} \parallel A}.U_{1}} & = &~ \xi \, \updatebig{\kappa}{\componentbbig{\kappa}{\dyn{P}} \parallel \dyn{A}}. \dyn{U_{1}}  \quad\text{with $\kappa = \ecs{\CStr(\component{a}{P})}$} & \\
%(3a)~ & \dyn{\update{a}{\component{a}{U} \parallel A}.U_{1}} & = &~ \sum_{\kappa \in \ecs{\proj{S}{a}} } 
%\updatebig{\kappa}{\componentbbig{\kappa}{\dyn{U}} \parallel \dyn{A}}.\dyn{U_{1}} & \text{if $C1$}\\
%(3b)~& \dyn{! \, \update{a}{\component{a}{U} \parallel A}.U_{1}} & = &~ \prod_{\kappa \in \ecs{\proj{S}{a}}}
%! \, \updatebig{\kappa}{\componentbbig{\kappa}{\dyn{U}} \parallel \dyn{A}}.\dyn{U_{1}} &  \text{if $C1$} \\
%(4)~& \dyn{\xi \, \update{a}{\component{a}{U} \parallel A}.U_{1}} & = &~ \xi \, \updatebig{\kappa}{\componentbbig{\kappa}{\dyn{U}} \parallel \dyn{A}}. \dyn{U_{1}} \quad \text{with $\kappa = \ecs{\CStr(\component{a}{U})}$} &  \text{if $C2$} \\
%(5)~& \dyn{\xi \, \update{a}{\component{a}{U} \parallel A}.U_{1}} &= &~ \xi \, \update{\mathrm{err}}{\nil}. \dyn{U_{1}} & \text{if $C3$} \\
%(6)~& \dyn{\xi \, \pi . U} & = &~ \xi \, \pi.\dyn{U}\quad \text{if $\pi = a$ or $\pi = \outC{a}$} & \\
%(7)~& \dyn{\sum_{i \in I} \pi_i.U_{i}} & = & ~\sum_{i \in I} \dyn{\pi_i. U_{i}} & \\
%(8)~& \dyn{U_{1} \parallel U_{2}} &= &~\dyn{U_{1}} \parallel \dyn{U_{2}} & \\
%(9)~& \dyn{\bullet} &= &~\bullet &
%\end{align*}
%\caption{\todo{needs fixes} The encoding $\dyn{\cdot}: \evols{}~\to~\evold{}$ given in Definition \ref{def:din}. 
%}\label{f:encsd}
%\end{figure}

% Version May 24
\begin{figure}
\linefigure
\begin{align*}
(1)~& \dyn{\component{a}{P}}&=&~\componentbbig{\kappa}{\dyn{P}}  \quad\text{with $\kappa = \ecs{\component{a}{P}}$} & \\
(2)~& \dyn{\xi \, \update{a}{\component{a}{U} \parallel A}.U_{1}}&=&~ \xi \, \updatebig{\kappa}{\componentbbig{\kappa}{\dyn{U}} \parallel \dyn{A}}. \dyn{U_{1}}\\
&&&\text{with $\kappa = \ecs{\component{a}{U}}$}& \text{if $C1$}  \\
(3)~& \dyn{\xi \, \update{a}{\component{a}{U} \parallel A}.U_{1}}&=&~ \xi \, \updatebig{\kappa_{a}}{\componentbbig{\kappa_{a}}{\dyn{U}} \parallel \dyn{A}}. \dyn{U_{1}}&  \text{if $C2$} \\
(3a)~& \dyn{\update{a}{\component{a}{U} \parallel A}.U_{1}} & = &~ \sum_{\kappa_{i} \in \ecs{\proj{S}{a}} } 
\updatebig{\kappa_{i}}{\componentbbig{\kappa_{i}}{\dyn{U}} \parallel \dyn{A}}.\dyn{U_{1}} & \text{if $C3$}\\
(3b)~& \dyn{! \, \update{a}{\component{a}{U} \parallel A}.U_{1}} & = &~ \prod_{\kappa_{i} \in \ecs{\proj{S}{a}}}
! \, \updatebig{\kappa_{i}}{\componentbbig{\kappa_{i}}{\dyn{U}} \parallel \dyn{A}}.\dyn{U_{1}} &  \text{if $C3$} \\
(5)~& \dyn{\xi \, \update{a}{\component{a}{U} \parallel A}.U_{1}}&=&~ \xi \, \update{\mathrm{err}}{\nil}. \dyn{U_{1}} & \text{if $C4$} \\
(6)~& \dyn{\xi \, \pi . U} & = &~ \xi \, \pi.\dyn{U}\quad \text{if $\pi = a$ or $\pi = \outC{a}$} & \\
(7)~& \dyn{\sum_{i \in I} \pi_i.U_{i}} & = & ~\sum_{i \in I} \dyn{\pi_i. U_{i}} & \\
(8)~& \dyn{U_{1} \parallel U_{2}} &= &~\dyn{U_{1}} \parallel \dyn{U_{2}} & \\
(9)~& \dyn{\bullet} &= &~\bullet &
\end{align*}
\small{Above, $\xi \pi.P$ denotes a possibly replicated prefixed process:
$\xi \pi.P$ is either $!\pi.P$ or $\pi.P$, with $\xi$ being the same on both sides of the definition.}
%We write $\xi \pi.P$ to denote a possibly replicated prefixed process, 
% that is, $\xi \pi.P$ denotes either $!\pi.P$ or $\pi.P$. $\xi$ is the same on both side of rules
\caption{The encoding $\dyn{\cdot}: \evols{}~\to~\evold{}$ given in Definition \ref{def:din}. 
}\label{f:encsd}
\linefigure
\end{figure}



%As for lines $(3a)$-$(3b)$ and $(4)$, it is immediate to observe the relationship between conditions  $C1$ and $C2$ 
%in the definition of  $\dyn{\cdot}$ and items (1) and (2) of  Lemma \ref{lem:statvsdyn}, respectively.

Before stating the correctness of the encoding, 
we illustrate it further  through a series of examples.

\begin{example} Below, notice that by virtue of Definition \ref{d:eccsstatic},  $\numap{A_{i}} = 0$ for every $A_{i}$.
\begin{enumerate}
\item Given the \evols{} process
$$P_{1} = \componentbbig{b}{\component{c}{A_{1} \parallel A_{2}}} \parallel \componentbbig{b}{\component{d}{e.A_{3}}} \parallel  \updatebig{b}{\component{c}{A_{4}}}.Q_{2}$$
we have the \evold{} process 
$$\dyn{P_{1}} = \componentbbig{\kappa_{1}}{\dyn{\component{c}{A_{1} \parallel A_{2}}}} \parallel \componentbbig{\kappa_{2}}{\dyn{\component{d}{e.A_{3}}}} \parallel  \updatebig{\kappa_{1}}{\dyn{\component{c}{A_{4}}}}.\dyn{Q_{2}}$$
with $\kappa_{1} = \ecs{\component{b}{\component{c}{A_{1} \parallel A_{2}}} }$ and $\kappa_{2} = \ecs{\component{b}{\component{d}{e.A_{3}}}}$.
 Notice how the renaming to $\kappa_{2}$
rules out the possibility of an update action for the second adaptable processes on $b$.

\item Given the \evols{} process
\begin{align*}
P_{2} = &\component{c}{A_{1}} \parallel \component{c}{A_{2}} \parallel \component{d}{A_{3}} \parallel \componentbbig{d}{\component{e}{A_{4}}} \parallel \\
& \update{c}{\component{c}{\bullet \parallel \bullet} \parallel A_{5}}.Q_{1} \parallel \update{d}{\component{d}{A_{6} \parallel a.\bullet}}.Q_{2}
\end{align*}
we have the \evold{} process 
\begin{align*}
\dyn{P_{2}} = &
\componentbbig{\kappa_c}{\dyn{A_{1}}} \parallel \componentbbig{\kappa_c}{\dyn{A_{2}}} \parallel \componentbbig{\kappa_d}{\dyn{A_{3}}} \parallel \componentbbig{\kappa_{1}}{\dyn{\component{e}{A_{4}}}} \parallel \\
& \updatebig{\kappa_c}{\component{\kappa_c}{\bullet \parallel \bullet} \parallel \dyn{A_{5}}}.\dyn{Q_{1}} \parallel \updatebig{\kappa_d}{\component{\kappa_d}{\dyn{A_{6}} \parallel a.\bullet}}.\dyn{Q_{2}}
\end{align*}
with $\kappa_{1} = \ecs{\component{d}{\component{e}{A_{4}}}}$. Notice how the renaming to $\kappa_{1}$
rules out the possibility of an update action for the second adaptable processes on $d$.


\item 
%\todo{change with Ai}
Given the \evols{} process $P_3$ defined as:
$$%P_{3} = 
\componentbbig{e}{\component{f}{A_{1}}} \parallel \componentbbig{e}{\component{g}{\component{h}{A_{2}} \parallel A_{3}}} \parallel (\updatebig{e}{\component{e}{\bullet} \parallel A_{4}}.Q_{1} \, + \, \updatebig{e}{\component{e}{\component{f}{\bullet \parallel \bullet}} \parallel A_{5}}.Q_{2})$$
we have (assuming $S$ to be minimal) the $\evold{}$ process
\begin{align*}
\dyn{P_{3}}  = & ~\componentbbig{\kappa_{1}}{\dyn{\component{f}{A_{1}}}} \parallel \componentbbig{\kappa_{2}}{\dyn{\component{g}{\component{h}{A_{2}} \parallel A_{3}}}} \parallel \\
& (\updatebig{\kappa_{1}}{\component{\kappa_{1}}{\bullet} \parallel \dyn{A_{4}}}.\dyn{Q_{1}} + 
 \updatebig{\kappa_{2}}{\component{\kappa_{2}}{\bullet} \parallel \dyn{A_{4}}}.\dyn{Q_{1}} + 
\update{\mathrm{err}}{\nil}.\dyn{Q_{2}})
\end{align*}
with $\kappa_{1}  = \ecs{\component{e}{\component{f}{A_{1}}}}$ and 
$\kappa_{2} = \ecs{\component{e}{\component{g}{\component{h}{A_{2}} \parallel A_{3}}} }$.\\
Observe how the first summand in $P_{3}$ has been duplicated in $\dyn{P_{3}}$, so as to account for the two possible update actions on $e$.
\end{enumerate}
\end{example}

We are in place to state the promised correspondence between \evols{} and \evold{} processes:

\begin{theorem}\label{stdynequiv}
Let $P$  be an \evols{} process.
Also, let $S$ be 
a set of containment structure denotations, such that  $\CStrs(P) \subseteq S$.
 Then we have:
$$P \pired_s P'\text{ if and only if }\dyn{P} \pired_d \dyns{P'}{S}$$
\end{theorem}
%\begin{proof}[Sketch]
\begin{proof}[Proof (Sketch)]
We divide the proof into two parts, one for the ``if'' direction and another other for the ``only if'' direction.
In both cases, we proceed 
by induction on the height of the derivation tree for $P \pired_{s} P'$ (resp. $\dyn{P} \pired_{d} \dyn{P'}$), with a case
analysis on the last applied rule.
For the former, we rely on the characterization of reduction for \evols{} processes given by Lemma \ref{lem:statvsdyn}
so as to show that a reduction in the static side is preserved in the dynamic side.
As for the latter, the proof is very similar, and exploits the fact that the encoding transforms update prefixes that may lead to incorrect update actions
into ``error'' update prefixes which are unable to participate in reductions. This ensures that for every dynamic reduction there is also a static reduction.
See \ref{ap:stdynequiv} in page \pageref{ap:stdynequiv} for details.
%\todo{prove this theorem}
\end{proof}


%\begin{definition}
%Let $P$ be an $\evols{}$ term and $P_1 \dots P_n$ be $\evols{}$ terms representing additional components 
%
%
%a set of component structure denotations
%such that $CStrs(P) \subseteq S$. We define $dyn_S(P)$ as the $\evold{}$ term (over $\mathcal{N}$ such that $S \cup \{err\} \subseteq \mathcal{N}$) inductively 
%obtained follows:




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
